Модальности в связаном Топосе

Для тех, кто попал сюда случайно, хочу напомнить, что необходимый прекурсор для этого журнала — "перинатальная топология" t.me/systemflow. Я и сам хотел всё это писать, но поскольку Адам, очевидно, ориентируется в математике лучше меня, оставляю для себя возможность писать более прозаически, помня о том, что большинство термов, про которые я говорю, находятся в репозитории groupoid/infinity. Желающие формальных определений могут уже ознакомиться с основами математики и программирования в виде 10 выпусков о гомотопической теории типов на сайте groupoid.space. Пока сформированы только 3 выпуска: 1-й (MLTT), 3-й (HoTT) и 8-й (Topoi). Почему я про них вспомнил, потому что сегодня речь пойдет о cohesive (связующих модальных) топосах, как важном расширении теории типов вообще и гомотопической теории типов в частности. Про cohesive топосы вы можете также прочитать у Адама в "перинатальной топологии", я же расширю это видение, чтобы читатель мог заняться компаративистикой, ведь два источника всегда лучше чем один!

Связующие модальные топосы были придуманы Ловером, как мощное средство построения сопряженных преобразований между теориями. Вообще, топосы — это про соединение категорной и топологической информации. Если быть формальным, то связанный топос — это геометрический морфизм, который генерирует сопряженную тройку модальных операторов

∫ (shape) ⊣ ♭(flat) ⊣ # (sharp).

Геометрический мортфизм — это пара функторов между категориями пучков, пучек — это предпучек с сайтом Гротендика, сайт Гротендика — это запакованная модель топологии через покрытия (я встречал в литературе три модели).

Предпучек — это просто функтор из обратной категории в категорию множеств! Тут впервые можно упомянуть зоопарк теорий множеств. Я же советую ознакомится только с тремя теориями множеств: ZFC, NBG, ETCS. Последняя теория — это категорная модель теории множеств построенная самим Ловером, чтобы пальцами можно было поводить по коммутативных диаграммах и показать что всё аксиомы теории множеств берутся из топоса.

Дифференциальный связующий топос — это топос с двумя такими сопряженными тройками. Если первая тройка относится к алгебраической топологии, то вторая тройка модальных операторов относится к дифференциальной геометрии. Левый модальный оператор первой тройки, shape модалити оператор, переводит теоретико-множественные геометрические места точек (например, для S^1 =_{SET} { (x,y) \in R \times R \| x^2 + y^2 = 1} ) в гомотопическую информацию (для окружности, например, S^1 =_{HIT} { base : S^1, loop: base = base }. Таким образом, можно сказать, что шейп оператор делает из множества групоид, вытаскивая информацию о группах из топологии покрытий, которая находится в топосах. Вот как в HoTT выглядит определение этого оператора и его рекурсор:

Где R — это модель вещественной прямой. Еще его называют фундаментальный инфинити групоид. Обратный оператор (бемоль или флэт модалити) соотвественно переводит из гомотопического определения (для чего HoTT и была придумана) в теоретико-множественное определение, наделяя это множество топологией, заданной покрытием, сформированным из гомотопической информации по HIT типу (или другими словами на основе его гомогенной структуры композиции). Если представить бемоль в теории типов, то ничего интересного не получится, так как это будет просто коиндуктивный процесс ретопологизации:

Один из примеров связующих топосов — это категории рефлексивных графов, как предпучок над категорией множеств. Если G — такой граф, то shape(G) — это граф компонентной связности G, flat(G) — это граф с теми же вершинами, что G, но только лишь с рефлексивными стрелками, sharp(G) — это полная сеть на множестве вершин графа G.

Теперь перейдем к дифференциальной геометории и тройке сопряженным модальных операторов связующего дифференциального топоса:

Средний модальный оператор — это коредукция, стек де Рама, или инфинитезимальная форма, она позволяет моделироват бесконечно-малые окресности вокруг точек, скрывая комонадические вычисления за 5 аксиомами теории типов: формация, интро, элиминатор, бета и эта правила. С ее помощью мы будем моделировать картановую геометрию в HoTT в следующих выпусках.

Про связующие топосы вы можете почитать в работах Уильяма Ловера, Майкла Шульмана, Урса Шрайбера, Феликса Веллена, Дэна Ликаты. Последние два также есть на youtube.